

LEMMA

If x partially overlaps y and y tangentially contains z, then x is not part of z.
=============================
Step 1

? (all x (all y (all z (((po x y) & (tpp-1 y z)) => (~ (p x z))))))


> revsk
=============================
Step 2

? (((~ (po c1104983 c1104982)) v (~ (tpp-1 c1104982 c1104981))) v (~ (p c1104983 c1104981)))


> hypdisj
=============================
Step 3

? (~ (p c1104983 c1104981))

1. (tpp-1 c1104982 c1104981)
2. (po c1104983 c1104982)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c (f1099930 c1104983 Var49 Var50) c1104983)
|
|1. (p c1104983 c1104981)
|2. (tpp-1 c1104982 c1104981)
|3. (po c1104983 c1104982)
|
|> ((c (f1099930 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 5
|
|? (~ (p c1104983 Var49))
|
|1. (~ (c (f1099930 c1104983 Var49 Var50) c1104983))
|2. (p c1104983 c1104981)
|3. (tpp-1 c1104982 c1104981)
|4. (po c1104983 c1104982)
|
|> ((~ (p X Y)) <-- (po X Y))
|=============================
|Step 6
|
|? (po c1104983 Var49)
|
|1. (p c1104983 Var49)
|2. (~ (c (f1099930 c1104983 Var49 Var50) c1104983))
|3. (p c1104983 c1104981)
|4. (tpp-1 c1104982 c1104981)
|5. (po c1104983 c1104982)
|
|> hyp
=============================
Step 7

? (~ (c (f1099930 c1104983 c1104982 Var50) c1104981))

1. (p c1104983 c1104981)
2. (tpp-1 c1104982 c1104981)
3. (po c1104983 c1104982)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 8
|
|? (p c1104981 Var56)
|
|1. (c (f1099930 c1104983 c1104982 Var50) c1104981)
|2. (p c1104983 c1104981)
|3. (tpp-1 c1104982 c1104981)
|4. (po c1104983 c1104982)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 9
|
|? (pp c1104981 Var56)
|
|1. (~ (p c1104981 Var56))
|2. (c (f1099930 c1104983 c1104982 Var50) c1104981)
|3. (p c1104983 c1104981)
|4. (tpp-1 c1104982 c1104981)
|5. (po c1104983 c1104982)
|
|> ((pp X Y) <-- (tpp X Y))
|=============================
|Step 10
|
|? (tpp c1104981 Var56)
|
|1. (~ (pp c1104981 Var56))
|2. (~ (p c1104981 Var56))
|3. (c (f1099930 c1104983 c1104982 Var50) c1104981)
|4. (p c1104983 c1104981)
|5. (tpp-1 c1104982 c1104981)
|6. (po c1104983 c1104982)
|
|> ((tpp Y X) <-- (tpp-1 X Y))
|=============================
|Step 11
|
|? (tpp-1 Var56 c1104981)
|
|1. (~ (tpp c1104981 Var56))
|2. (~ (pp c1104981 Var56))
|3. (~ (p c1104981 Var56))
|4. (c (f1099930 c1104983 c1104982 Var50) c1104981)
|5. (p c1104983 c1104981)
|6. (tpp-1 c1104982 c1104981)
|7. (po c1104983 c1104982)
|
|> hyp
=============================
Step 12

? (~ (c (f1099930 c1104983 c1104982 Var50) c1104982))

1. (c (f1099930 c1104983 c1104982 Var50) c1104981)
2. (p c1104983 c1104981)
3. (tpp-1 c1104982 c1104981)
4. (po c1104983 c1104982)

> ((~ (c (f1099930 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 13

? (~ (p c1104983 c1104982))

1. (c (f1099930 c1104983 c1104982 Var50) c1104982)
2. (c (f1099930 c1104983 c1104982 Var50) c1104981)
3. (p c1104983 c1104981)
4. (tpp-1 c1104982 c1104981)
5. (po c1104983 c1104982)

> ((~ (p X Y)) <-- (po X Y))
=============================
Step 14

? (po c1104983 c1104982)

1. (p c1104983 c1104982)
2. (c (f1099930 c1104983 c1104982 Var50) c1104982)
3. (c (f1099930 c1104983 c1104982 Var50) c1104981)
4. (p c1104983 c1104981)
5. (tpp-1 c1104982 c1104981)
6. (po c1104983 c1104982)

> hyp


LEMMA

Partial overlap implies overlap.
=============================
Step 1

? (all x (all y ((po x y) => (o x y))))


> revsk
=============================
Step 2

? ((~ (po c1110212 c1110211)) v (o c1110212 c1110211))


> hypdisj
=============================
Step 3

? (o c1110212 c1110211)

1. (po c1110212 c1110211)

> ((o X Y) <-- (po X Y))
=============================
Step 4

? (po c1110212 c1110211)

1. (~ (o c1110212 c1110211))
2. (po c1110212 c1110211)

> hyp


LEMMA

Overlap implies connection.
=============================
Step 1

? (all x (all y ((o x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (o c1115497 c1115496)) v (c c1115497 c1115496))


> hypdisj
=============================
Step 3

? (c c1115497 c1115496)

1. (o c1115497 c1115496)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var48 c1115496)
|
|1. (~ (c c1115497 c1115496))
|2. (o c1115497 c1115496)
|
|> ((p Z X) <-- (~ (c (f1110244 Z X Y) Z)))
|=============================
|Step 5
|
|? (~ (c (f1110244 Var48 c1115496 Var51) Var48))
|
|1. (~ (p Var48 c1115496))
|2. (~ (c c1115497 c1115496))
|3. (o c1115497 c1115496)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 6
||
||? (p (f1110261 Var57 Var54) Var54)
||
||1. (c (f1110244 (f1110261 Var57 Var54) c1115496 Var51) (f1110261 Var57 Var54))
||2. (~ (p (f1110261 Var57 Var54) c1115496))
||3. (~ (c c1115497 c1115496))
||4. (o c1115497 c1115496)
||
||> ((p (f1110261 X Y) Y) <-- (o X Y))
||=============================
||Step 7
||
||? (o Var57 Var54)
||
||1. (~ (p (f1110261 Var57 Var54) Var54))
||2. (c (f1110244 (f1110261 Var57 Var54) c1115496 Var51) (f1110261 Var57 Var54))
||3. (~ (p (f1110261 Var57 Var54) c1115496))
||4. (~ (c c1115497 c1115496))
||5. (o c1115497 c1115496)
||
||> hyp
|=============================
|Step 8
|
|? (~ (c (f1110244 (f1110261 c1115497 c1115496) c1115496 Var51) c1115496))
|
|1. (c (f1110244 (f1110261 c1115497 c1115496) c1115496 Var51) (f1110261 c1115497 c1115496))
|2. (~ (p (f1110261 c1115497 c1115496) c1115496))
|3. (~ (c c1115497 c1115496))
|4. (o c1115497 c1115496)
|
|> ((~ (c (f1110244 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p (f1110261 c1115497 c1115496) c1115496))
|
|1. (c (f1110244 (f1110261 c1115497 c1115496) c1115496 Var51) c1115496)
|2. (c (f1110244 (f1110261 c1115497 c1115496) c1115496 Var51) (f1110261 c1115497 c1115496))
|3. (~ (p (f1110261 c1115497 c1115496) c1115496))
|4. (~ (c c1115497 c1115496))
|5. (o c1115497 c1115496)
|
|> hyp
=============================
Step 10

? (c c1115497 (f1110261 c1115497 c1115496))

1. (~ (c c1115497 c1115496))
2. (o c1115497 c1115496)

> ((c Y X) <-- (c X Y))
=============================
Step 11

? (c (f1110261 c1115497 c1115496) c1115497)

1. (~ (c c1115497 (f1110261 c1115497 c1115496)))
2. (~ (c c1115497 c1115496))
3. (o c1115497 c1115496)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 12
|
|? (p (f1110261 c1115497 Var71) c1115497)
|
|1. (~ (c (f1110261 c1115497 c1115496) c1115497))
|2. (~ (c c1115497 (f1110261 c1115497 c1115496)))
|3. (~ (c c1115497 c1115496))
|4. (o c1115497 c1115496)
|
|> ((p (f1110261 X Y) X) <-- (o X Y))
|=============================
|Step 13
|
|? (o c1115497 Var71)
|
|1. (~ (p (f1110261 c1115497 Var71) c1115497))
|2. (~ (c (f1110261 c1115497 c1115496) c1115497))
|3. (~ (c c1115497 (f1110261 c1115497 c1115496)))
|4. (~ (c c1115497 c1115496))
|5. (o c1115497 c1115496)
|
|> hyp
=============================
Step 14

? (c (f1110261 c1115497 c1115496) (f1110261 c1115497 c1115496))

1. (~ (c (f1110261 c1115497 c1115496) c1115497))
2. (~ (c c1115497 (f1110261 c1115497 c1115496)))
3. (~ (c c1115497 c1115496))
4. (o c1115497 c1115496)

> ((c X X) <--)


LEMMA

Inverse tangential proper part implies inverse proper part.
=============================
Step 1

? (all x (all y ((tpp-1 x y) => (pp-1 x y))))


> revsk
=============================
Step 2

? ((~ (tpp-1 c1120838 c1120837)) v (pp-1 c1120838 c1120837))


> hypdisj
=============================
Step 3

? (pp-1 c1120838 c1120837)

1. (tpp-1 c1120838 c1120837)

> ((pp-1 Y X) <-- (pp X Y))
=============================
Step 4

? (pp c1120837 c1120838)

1. (~ (pp-1 c1120838 c1120837))
2. (tpp-1 c1120838 c1120837)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 5

? (tpp c1120837 c1120838)

1. (~ (pp c1120837 c1120838))
2. (~ (pp-1 c1120838 c1120837))
3. (tpp-1 c1120838 c1120837)

> ((tpp Y X) <-- (tpp-1 X Y))
=============================
Step 6

? (tpp-1 c1120838 c1120837)

1. (~ (tpp c1120837 c1120838))
2. (~ (pp c1120837 c1120838))
3. (~ (pp-1 c1120838 c1120837))
4. (tpp-1 c1120838 c1120837)

> hyp


LEMMA

Inverse proper part implies inverse parthood.
=============================
Step 1

? (all x (all y ((pp-1 x y) => (p-1 x y))))


> revsk
=============================
Step 2

? ((~ (pp-1 c1126235 c1126234)) v (p-1 c1126235 c1126234))


> hypdisj
=============================
Step 3

? (p-1 c1126235 c1126234)

1. (pp-1 c1126235 c1126234)

> ((p-1 Y X) <-- (p X Y))
=============================
Step 4

? (p c1126234 c1126235)

1. (~ (p-1 c1126235 c1126234))
2. (pp-1 c1126235 c1126234)

> ((p X Y) <-- (pp X Y))
=============================
Step 5

? (pp c1126234 c1126235)

1. (~ (p c1126234 c1126235))
2. (~ (p-1 c1126235 c1126234))
3. (pp-1 c1126235 c1126234)

> ((pp Y X) <-- (pp-1 X Y))
=============================
Step 6

? (pp-1 c1126235 c1126234)

1. (~ (pp c1126234 c1126235))
2. (~ (p c1126234 c1126235))
3. (~ (p-1 c1126235 c1126234))
4. (pp-1 c1126235 c1126234)

> hyp


LEMMA

Parthood transports connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c1131690 c1131689)) v (~ (c c1131688 c1131690))) v (c c1131688 c1131689))


> hypdisj
=============================
Step 3

? (c c1131688 c1131689)

1. (c c1131688 c1131690)
2. (p c1131690 c1131689)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c1131689)
|
|1. (~ (c c1131688 c1131689))
|2. (c c1131688 c1131690)
|3. (p c1131690 c1131689)
|
|> hyp
=============================
Step 5

? (c c1131688 c1131690)

1. (~ (c c1131688 c1131689))
2. (c c1131688 c1131690)
3. (p c1131690 c1131689)

> hyp


LEMMA

Split x,z into disconnection or connection.
=============================
Step 1

? (all x (all y (all z (((po x y) & (tpp-1 y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (po c1137301 c1137300)) v (~ (tpp-1 c1137300 c1137299))) v ((dc c1137301 c1137299) v (c c1137301 c1137299)))


> hypdisj
=============================
Step 3

? (c c1137301 c1137299)

1. (~ (dc c1137301 c1137299))
2. (tpp-1 c1137300 c1137299)
3. (po c1137301 c1137300)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c1137301 c1137299))

1. (~ (c c1137301 c1137299))
2. (~ (dc c1137301 c1137299))
3. (tpp-1 c1137300 c1137299)
4. (po c1137301 c1137300)

> hyp


LEMMA

In the connected case, x,z are ec or po or z is part of x.
=============================
Step 1

? (all x (all y (all z ((((po x y) & (tpp-1 y z)) & (c x z)) => (((ec x z) v (po x z)) v (p z x))))))


> revsk
=============================
Step 2

? ((((~ (po c1143178 c1143177)) v (~ (tpp-1 c1143177 c1143176))) v (~ (c c1143178 c1143176))) v (((ec c1143178 c1143176) v (po c1143178 c1143176)) v (p c1143176 c1143178)))


> hypdisj
=============================
Step 3

? (p c1143176 c1143178)

1. (~ (po c1143178 c1143176))
2. (~ (ec c1143178 c1143176))
3. (c c1143178 c1143176)
4. (tpp-1 c1143177 c1143176)
5. (po c1143178 c1143177)

> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||=============================
||Step 4
||
||? (o c1143178 c1143176)
||
||1. (~ (p c1143176 c1143178))
||2. (~ (po c1143178 c1143176))
||3. (~ (ec c1143178 c1143176))
||4. (c c1143178 c1143176)
||5. (tpp-1 c1143177 c1143176)
||6. (po c1143178 c1143177)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 5
|||
|||? (c c1143178 c1143176)
|||
|||1. (~ (o c1143178 c1143176))
|||2. (~ (p c1143176 c1143178))
|||3. (~ (po c1143178 c1143176))
|||4. (~ (ec c1143178 c1143176))
|||5. (c c1143178 c1143176)
|||6. (tpp-1 c1143177 c1143176)
|||7. (po c1143178 c1143177)
|||
|||> hyp
||=============================
||Step 6
||
||? (~ (ec c1143178 c1143176))
||
||1. (~ (o c1143178 c1143176))
||2. (~ (p c1143176 c1143178))
||3. (~ (po c1143178 c1143176))
||4. (~ (ec c1143178 c1143176))
||5. (c c1143178 c1143176)
||6. (tpp-1 c1143177 c1143176)
||7. (po c1143178 c1143177)
||
||> hyp
|=============================
|Step 7
|
|? (~ (p c1143178 c1143176))
|
|1. (~ (p c1143176 c1143178))
|2. (~ (po c1143178 c1143176))
|3. (~ (ec c1143178 c1143176))
|4. (c c1143178 c1143176)
|5. (tpp-1 c1143177 c1143176)
|6. (po c1143178 c1143177)
|
|> ((~ (p X Z)) <-- (po X Y) (tpp-1 Y Z))
||=============================
||Step 8
||
||? (po c1143178 Var37)
||
||1. (p c1143178 c1143176)
||2. (~ (p c1143176 c1143178))
||3. (~ (po c1143178 c1143176))
||4. (~ (ec c1143178 c1143176))
||5. (c c1143178 c1143176)
||6. (tpp-1 c1143177 c1143176)
||7. (po c1143178 c1143177)
||
||> hyp
|=============================
|Step 9
|
|? (tpp-1 c1143177 c1143176)
|
|1. (p c1143178 c1143176)
|2. (~ (p c1143176 c1143178))
|3. (~ (po c1143178 c1143176))
|4. (~ (ec c1143178 c1143176))
|5. (c c1143178 c1143176)
|6. (tpp-1 c1143177 c1143176)
|7. (po c1143178 c1143177)
|
|> hyp
=============================
Step 10

? (~ (po c1143178 c1143176))

1. (~ (p c1143176 c1143178))
2. (~ (po c1143178 c1143176))
3. (~ (ec c1143178 c1143176))
4. (c c1143178 c1143176)
5. (tpp-1 c1143177 c1143176)
6. (po c1143178 c1143177)

> hyp


LEMMA

Converse parthood plus failure of forward parthood gives inverse proper part.
=============================
Step 1

? (all x (all y (((p y x) & (~ (p x y))) => (pp-1 x y))))


> revsk
=============================
Step 2

? (((~ (p c1149664 c1149665)) v (p c1149665 c1149664)) v (pp-1 c1149665 c1149664))


> hypdisj
=============================
Step 3

? (pp-1 c1149665 c1149664)

1. (~ (p c1149665 c1149664))
2. (p c1149664 c1149665)

> ((pp-1 Y X) <-- (pp X Y))
=============================
Step 4

? (pp c1149664 c1149665)

1. (~ (pp-1 c1149665 c1149664))
2. (~ (p c1149665 c1149664))
3. (p c1149664 c1149665)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 5
|
|? (p c1149664 c1149665)
|
|1. (~ (pp c1149664 c1149665))
|2. (~ (pp-1 c1149665 c1149664))
|3. (~ (p c1149665 c1149664))
|4. (p c1149664 c1149665)
|
|> hyp
=============================
Step 6

? (~ (p c1149665 c1149664))

1. (~ (pp c1149664 c1149665))
2. (~ (pp-1 c1149665 c1149664))
3. (~ (p c1149665 c1149664))
4. (p c1149664 c1149665)

> hyp


LEMMA

Inverse proper part splits into tangential or non-tangential inverse proper part.
=============================
Step 1

? (all x (all y ((pp-1 x y) => ((tpp-1 x y) v (ntpp-1 x y)))))


> revsk
=============================
Step 2

? ((~ (pp-1 c1156303 c1156302)) v ((tpp-1 c1156303 c1156302) v (ntpp-1 c1156303 c1156302)))


> hypdisj
=============================
Step 3

? (ntpp-1 c1156303 c1156302)

1. (~ (tpp-1 c1156303 c1156302))
2. (pp-1 c1156303 c1156302)

> ((ntpp-1 Y X) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c1156302 c1156303)

1. (~ (ntpp-1 c1156303 c1156302))
2. (~ (tpp-1 c1156303 c1156302))
3. (pp-1 c1156303 c1156302)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f1149780 Z X Y) Z)))
|=============================
|Step 5
|
|? (pp c1156302 c1156303)
|
|1. (~ (ntpp c1156302 c1156303))
|2. (~ (ntpp-1 c1156303 c1156302))
|3. (~ (tpp-1 c1156303 c1156302))
|4. (pp-1 c1156303 c1156302)
|
|> ((pp Y X) <-- (pp-1 X Y))
|=============================
|Step 6
|
|? (pp-1 c1156303 c1156302)
|
|1. (~ (pp c1156302 c1156303))
|2. (~ (ntpp c1156302 c1156303))
|3. (~ (ntpp-1 c1156303 c1156302))
|4. (~ (tpp-1 c1156303 c1156302))
|5. (pp-1 c1156303 c1156302)
|
|> hyp
=============================
Step 7

? (~ (ec (f1149780 c1156302 c1156303 Var44) c1156302))

1. (~ (ntpp c1156302 c1156303))
2. (~ (ntpp-1 c1156303 c1156302))
3. (~ (tpp-1 c1156303 c1156302))
4. (pp-1 c1156303 c1156302)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 8
||
||? (pp c1156302 Var50)
||
||1. (ec (f1149780 c1156302 c1156303 Var44) c1156302)
||2. (~ (ntpp c1156302 c1156303))
||3. (~ (ntpp-1 c1156303 c1156302))
||4. (~ (tpp-1 c1156303 c1156302))
||5. (pp-1 c1156303 c1156302)
||
||> ((pp Y X) <-- (pp-1 X Y))
||=============================
||Step 9
||
||? (pp-1 Var50 c1156302)
||
||1. (~ (pp c1156302 Var50))
||2. (ec (f1149780 c1156302 c1156303 Var44) c1156302)
||3. (~ (ntpp c1156302 c1156303))
||4. (~ (ntpp-1 c1156303 c1156302))
||5. (~ (tpp-1 c1156303 c1156302))
||6. (pp-1 c1156303 c1156302)
||
||> hyp
|=============================
|Step 10
|
|? (ec (f1149780 c1156302 c1156303 Var44) c1156303)
|
|1. (ec (f1149780 c1156302 c1156303 Var44) c1156302)
|2. (~ (ntpp c1156302 c1156303))
|3. (~ (ntpp-1 c1156303 c1156302))
|4. (~ (tpp-1 c1156303 c1156302))
|5. (pp-1 c1156303 c1156302)
|
|> ((ec (f1149780 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 11
||
||? (~ (ntpp c1156302 c1156303))
||
||1. (~ (ec (f1149780 c1156302 c1156303 Var44) c1156303))
||2. (ec (f1149780 c1156302 c1156303 Var44) c1156302)
||3. (~ (ntpp c1156302 c1156303))
||4. (~ (ntpp-1 c1156303 c1156302))
||5. (~ (tpp-1 c1156303 c1156302))
||6. (pp-1 c1156303 c1156302)
||
||> hyp
|=============================
|Step 12
|
|? (pp c1156302 c1156303)
|
|1. (~ (ec (f1149780 c1156302 c1156303 Var44) c1156303))
|2. (ec (f1149780 c1156302 c1156303 Var44) c1156302)
|3. (~ (ntpp c1156302 c1156303))
|4. (~ (ntpp-1 c1156303 c1156302))
|5. (~ (tpp-1 c1156303 c1156302))
|6. (pp-1 c1156303 c1156302)
|
|> ((pp Y X) <-- (pp-1 X Y))
|=============================
|Step 13
|
|? (pp-1 c1156303 c1156302)
|
|1. (~ (pp c1156302 c1156303))
|2. (~ (ec (f1149780 c1156302 c1156303 Var44) c1156303))
|3. (ec (f1149780 c1156302 c1156303 Var44) c1156302)
|4. (~ (ntpp c1156302 c1156303))
|5. (~ (ntpp-1 c1156303 c1156302))
|6. (~ (tpp-1 c1156303 c1156302))
|7. (pp-1 c1156303 c1156302)
|
|> hyp
=============================
Step 14

? (~ (tpp c1156302 c1156303))

1. (ec (f1149780 c1156302 c1156303 Var44) c1156302)
2. (~ (ntpp c1156302 c1156303))
3. (~ (ntpp-1 c1156303 c1156302))
4. (~ (tpp-1 c1156303 c1156302))
5. (pp-1 c1156303 c1156302)

> ((~ (tpp Y X)) <-- (~ (tpp-1 X Y)))
=============================
Step 15

? (~ (tpp-1 c1156303 c1156302))

1. (tpp c1156302 c1156303)
2. (ec (f1149780 c1156302 c1156303 Var44) c1156302)
3. (~ (ntpp c1156302 c1156303))
4. (~ (ntpp-1 c1156303 c1156302))
5. (~ (tpp-1 c1156303 c1156302))
6. (pp-1 c1156303 c1156302)

> hyp


LEMMA

Split into dc(x,z) or c(x,z). In the connected case use Lemma8. If p(z,x), combine with Lemma1 to get pp-1(x,z), then Lemma10 gives tpp-1(x,z) or ntpp-1(x,z).
=============================
Step 1

? (all x (all y (all z (((po x y) & (tpp-1 y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp-1 x z)) v (ntpp-1 x z))))))


> revsk
=============================
Step 2

? (((~ (po c1163094 c1163093)) v (~ (tpp-1 c1163093 c1163092))) v (((((dc c1163094 c1163092) v (ec c1163094 c1163092)) v (po c1163094 c1163092)) v (tpp-1 c1163094 c1163092)) v (ntpp-1 c1163094 c1163092)))


> hypdisj
=============================
Step 3

? (ntpp-1 c1163094 c1163092)

1. (~ (tpp-1 c1163094 c1163092))
2. (~ (po c1163094 c1163092))
3. (~ (ec c1163094 c1163092))
4. (~ (dc c1163094 c1163092))
5. (tpp-1 c1163093 c1163092)
6. (po c1163094 c1163093)

> ((ntpp-1 X Y) <-- (pp-1 X Y) (~ (tpp-1 X Y)))
|=============================
|Step 4
|
|? (pp-1 c1163094 c1163092)
|
|1. (~ (ntpp-1 c1163094 c1163092))
|2. (~ (tpp-1 c1163094 c1163092))
|3. (~ (po c1163094 c1163092))
|4. (~ (ec c1163094 c1163092))
|5. (~ (dc c1163094 c1163092))
|6. (tpp-1 c1163093 c1163092)
|7. (po c1163094 c1163093)
|
|> ((pp-1 X Y) <-- (p Y X) (~ (p X Y)))
||=============================
||Step 5
||
||? (p c1163092 c1163094)
||
||1. (~ (pp-1 c1163094 c1163092))
||2. (~ (ntpp-1 c1163094 c1163092))
||3. (~ (tpp-1 c1163094 c1163092))
||4. (~ (po c1163094 c1163092))
||5. (~ (ec c1163094 c1163092))
||6. (~ (dc c1163094 c1163092))
||7. (tpp-1 c1163093 c1163092)
||8. (po c1163094 c1163093)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c1163094 c1163092)
||||
||||1. (~ (p c1163092 c1163094))
||||2. (~ (pp-1 c1163094 c1163092))
||||3. (~ (ntpp-1 c1163094 c1163092))
||||4. (~ (tpp-1 c1163094 c1163092))
||||5. (~ (po c1163094 c1163092))
||||6. (~ (ec c1163094 c1163092))
||||7. (~ (dc c1163094 c1163092))
||||8. (tpp-1 c1163093 c1163092)
||||9. (po c1163094 c1163093)
||||
||||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||||=============================
|||||Step 7
|||||
|||||? (c c1163094 c1163092)
|||||
|||||1. (~ (o c1163094 c1163092))
|||||2. (~ (p c1163092 c1163094))
|||||3. (~ (pp-1 c1163094 c1163092))
|||||4. (~ (ntpp-1 c1163094 c1163092))
|||||5. (~ (tpp-1 c1163094 c1163092))
|||||6. (~ (po c1163094 c1163092))
|||||7. (~ (ec c1163094 c1163092))
|||||8. (~ (dc c1163094 c1163092))
|||||9. (tpp-1 c1163093 c1163092)
|||||10. (po c1163094 c1163093)
|||||
|||||> ((c X Y) <-- (~ (dc X Y)))
|||||=============================
|||||Step 8
|||||
|||||? (~ (dc c1163094 c1163092))
|||||
|||||1. (~ (c c1163094 c1163092))
|||||2. (~ (o c1163094 c1163092))
|||||3. (~ (p c1163092 c1163094))
|||||4. (~ (pp-1 c1163094 c1163092))
|||||5. (~ (ntpp-1 c1163094 c1163092))
|||||6. (~ (tpp-1 c1163094 c1163092))
|||||7. (~ (po c1163094 c1163092))
|||||8. (~ (ec c1163094 c1163092))
|||||9. (~ (dc c1163094 c1163092))
|||||10. (tpp-1 c1163093 c1163092)
|||||11. (po c1163094 c1163093)
|||||
|||||> hyp
||||=============================
||||Step 9
||||
||||? (~ (ec c1163094 c1163092))
||||
||||1. (~ (o c1163094 c1163092))
||||2. (~ (p c1163092 c1163094))
||||3. (~ (pp-1 c1163094 c1163092))
||||4. (~ (ntpp-1 c1163094 c1163092))
||||5. (~ (tpp-1 c1163094 c1163092))
||||6. (~ (po c1163094 c1163092))
||||7. (~ (ec c1163094 c1163092))
||||8. (~ (dc c1163094 c1163092))
||||9. (tpp-1 c1163093 c1163092)
||||10. (po c1163094 c1163093)
||||
||||> hyp
|||=============================
|||Step 10
|||
|||? (~ (p c1163094 c1163092))
|||
|||1. (~ (p c1163092 c1163094))
|||2. (~ (pp-1 c1163094 c1163092))
|||3. (~ (ntpp-1 c1163094 c1163092))
|||4. (~ (tpp-1 c1163094 c1163092))
|||5. (~ (po c1163094 c1163092))
|||6. (~ (ec c1163094 c1163092))
|||7. (~ (dc c1163094 c1163092))
|||8. (tpp-1 c1163093 c1163092)
|||9. (po c1163094 c1163093)
|||
|||> ((~ (p X Z)) <-- (po X Y) (tpp-1 Y Z))
||||=============================
||||Step 11
||||
||||? (po c1163094 Var55)
||||
||||1. (p c1163094 c1163092)
||||2. (~ (p c1163092 c1163094))
||||3. (~ (pp-1 c1163094 c1163092))
||||4. (~ (ntpp-1 c1163094 c1163092))
||||5. (~ (tpp-1 c1163094 c1163092))
||||6. (~ (po c1163094 c1163092))
||||7. (~ (ec c1163094 c1163092))
||||8. (~ (dc c1163094 c1163092))
||||9. (tpp-1 c1163093 c1163092)
||||10. (po c1163094 c1163093)
||||
||||> hyp
|||=============================
|||Step 12
|||
|||? (tpp-1 c1163093 c1163092)
|||
|||1. (p c1163094 c1163092)
|||2. (~ (p c1163092 c1163094))
|||3. (~ (pp-1 c1163094 c1163092))
|||4. (~ (ntpp-1 c1163094 c1163092))
|||5. (~ (tpp-1 c1163094 c1163092))
|||6. (~ (po c1163094 c1163092))
|||7. (~ (ec c1163094 c1163092))
|||8. (~ (dc c1163094 c1163092))
|||9. (tpp-1 c1163093 c1163092)
|||10. (po c1163094 c1163093)
|||
|||> hyp
||=============================
||Step 13
||
||? (~ (po c1163094 c1163092))
||
||1. (~ (p c1163092 c1163094))
||2. (~ (pp-1 c1163094 c1163092))
||3. (~ (ntpp-1 c1163094 c1163092))
||4. (~ (tpp-1 c1163094 c1163092))
||5. (~ (po c1163094 c1163092))
||6. (~ (ec c1163094 c1163092))
||7. (~ (dc c1163094 c1163092))
||8. (tpp-1 c1163093 c1163092)
||9. (po c1163094 c1163093)
||
||> hyp
|=============================
|Step 14
|
|? (~ (p c1163094 c1163092))
|
|1. (~ (pp-1 c1163094 c1163092))
|2. (~ (ntpp-1 c1163094 c1163092))
|3. (~ (tpp-1 c1163094 c1163092))
|4. (~ (po c1163094 c1163092))
|5. (~ (ec c1163094 c1163092))
|6. (~ (dc c1163094 c1163092))
|7. (tpp-1 c1163093 c1163092)
|8. (po c1163094 c1163093)
|
|> ((~ (p X Z)) <-- (po X Y) (tpp-1 Y Z))
||=============================
||Step 15
||
||? (po c1163094 Var61)
||
||1. (p c1163094 c1163092)
||2. (~ (pp-1 c1163094 c1163092))
||3. (~ (ntpp-1 c1163094 c1163092))
||4. (~ (tpp-1 c1163094 c1163092))
||5. (~ (po c1163094 c1163092))
||6. (~ (ec c1163094 c1163092))
||7. (~ (dc c1163094 c1163092))
||8. (tpp-1 c1163093 c1163092)
||9. (po c1163094 c1163093)
||
||> hyp
|=============================
|Step 16
|
|? (tpp-1 c1163093 c1163092)
|
|1. (p c1163094 c1163092)
|2. (~ (pp-1 c1163094 c1163092))
|3. (~ (ntpp-1 c1163094 c1163092))
|4. (~ (tpp-1 c1163094 c1163092))
|5. (~ (po c1163094 c1163092))
|6. (~ (ec c1163094 c1163092))
|7. (~ (dc c1163094 c1163092))
|8. (tpp-1 c1163093 c1163092)
|9. (po c1163094 c1163093)
|
|> hyp
=============================
Step 17

? (~ (tpp-1 c1163094 c1163092))

1. (~ (ntpp-1 c1163094 c1163092))
2. (~ (tpp-1 c1163094 c1163092))
3. (~ (po c1163094 c1163092))
4. (~ (ec c1163094 c1163092))
5. (~ (dc c1163094 c1163092))
6. (tpp-1 c1163093 c1163092)
7. (po c1163094 c1163093)

> hyp
